es:ES, p:(E(E + Top)), a, b, c:E. a p< b  b p< c  a p< c 

latex

Definitions	x:A. B(x), P  Q, e p< e', x:A. B(x), t  T, , p-graph(A;f), A c B, P & Q, Top, S  T, suptype(S; T), do-apply(f;x), , P  Q, P  Q
Lemmas	nat plus wf, p-graph wf2, es-E wf, p-fun-exp wf, nat plus inc, top wf, event system wf, can-apply-fun-exp-add-iff, assert wf, can-apply wf, p-fun-exp-add-sq, can-apply-fun-exp, do-apply wf